Nuprl Lemma : retraction-fun-path 11,40

T:Type, f:(TT), h:(T).
(x:T. (f(x) = x ((h(f(x))) < (h(x))))
 (L:(T List), xy:Ty=f*(x) via L  ((x = y ((h(y)) < (h(x))))) 
latex


Definitionst  T, type List, A List, s = t, x:AB(x), x:AB(x), [car / cdr], y=f*(x) via L, Type, left + right, P  Q, f(a), a < b, P  Q, , [], {x:AB(x)} , , |g|, S  T, last(L), x:A  B(x), P & Q, hd(l), {T}, Void, P  Q, False, A, Dec(P), A  B, b, x:AB(x), b | a, a ~ b, a  b, a <p b, a < b, A c B, x f y, xLP(x), (xL.P(x)), ||as||, #$n, i  j , , , <ab>
Lemmashd wf, decidable lt, length wf1, fun-path-cons, nat wf, fun-path wf

origin